;;; -*- Mode: Lisp; Syntax: Common-Lisp; Package: snark -*-
;;; File: tptp.lisp
;;; The contents of this file are subject to the Mozilla Public License
;;; Version 1.1 (the "License"); you may not use this file except in
;;; compliance with the License. You may obtain a copy of the License at
;;; http://www.mozilla.org/MPL/
;;;
;;; Software distributed under the License is distributed on an "AS IS"
;;; basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See the
;;; License for the specific language governing rights and limitations
;;; under the License.
;;;
;;; The Original Code is SNARK.
;;; The Initial Developer of the Original Code is SRI International.
;;; Portions created by the Initial Developer are Copyright (C) 1981-2006.
;;; All Rights Reserved.
;;;
;;; Contributor(s): Mark E. Stickel <stickel@ai.sri.com>.

(in-package :snark)

;;; TSTP justifications are incomplete:
;;;   source files aren't named
;;;   cnf and other transformations aren't named
;;;   use of AC, other theories aren't named
;;;   in (rewrite assertion ...), assertion isn't named
;;; this information isn't present in the SNARK justification either

(defun print-row-in-tptp-format (row)
  (print-wff-in-tptp-format1 (row-wff row) (row-name-or-number row) (row-reason row))
  row)

(defun print-wff-in-tptp-format1 (wff name-or-number reason)
  (let ((clausep (clause-p wff nil t)))
    (when (and name-or-number reason)
      (princ (if clausep "cnf(" "fof("))
      (print-row-name-or-number-in-tptp-format name-or-number)
      (princ ", ")
      (print-row-reason-in-tptp-format reason)
      (princ ", ")
      (terpri)
      (princ "    "))
    (cond
     ((and clausep (neq true wff) (neq false wff))
      (prog->
        (literal-p wff :pos t -> atom polarity)
        (cond
         (atom
          (print-term-in-tptp-format atom nil (eq :neg polarity)))
         (t
          (prog->
            (quote t -> first)
            (map-atoms-in-clause wff ->* atom polarity)
            (if first (setf first nil) (princ " | "))
            (print-term-in-tptp-format atom nil (eq :neg polarity)))))))
     (t
      (print-wff-in-tptp-format wff)))
    (when (and name-or-number reason)
      (print-row-reason-in-tptp-format2 reason)
      (princ ")"))
    (princ ". ")
    wff))

(defun print-row-name-or-number-in-tptp-format (name-or-number)
  (etypecase name-or-number
    (number
     (write name-or-number :radix nil :base 10))
    (symbol
     (print-symbol-in-tptp-format name-or-number))))

(defun print-row-reason-in-tptp-format (reason)
  (princ (case reason
           (assertion "axiom")
           (assumption "hypothesis")
           (conjecture "conjecture")
           (negated_conjecture "negated_conjecture")
           (hint "hint")
           (otherwise "plain"))))

(defun print-row-reason-in-tptp-format2 (reason)
  (case reason
    ((assertion assumption conjecture negated_conjecture hint)
     )
    (otherwise
     (princ ",")
     (terpri)
     (princ "    ")
     (print-row-reason-in-tptp-format3 reason))))

(defun print-row-reason-in-tptp-format3 (x)
  (cond
   ((consp x)
    (princ "inference(")
    (cond
     ((eq 'paramodulate (first x))
      (setf x (append x '(|theory(equality)|))))
     ((eq 'rewrite (first x))
      (cond
       ((member :code-for-= (rest (rest x)))
        (setf x (append (remove :code-for-= x) '(|theory(equality)|))))
       ((some (lambda (row) (and (row-p row) (compound-p (row-wff row)) (eq *=* (head (row-wff row))))) (rest (rest x)))
        (setf x (append x '(|theory(equality)|)))))))
    (print-symbol-in-tptp-format (first x))
    (princ ",")
    (princ "[status(thm)]")
    (princ ",")
    (princ "[")
    (let ((first t))
      (dolist (arg (rest x))
        (if first (setf first nil) (princ ","))
        (print-row-reason-in-tptp-format3 arg)))
    (princ "]")
    (princ ")"))
   ((row-p x)
    (print-row-name-or-number-in-tptp-format (row-name-or-number x)))
   ((eq '|theory(equality)| x)
    (princ x))
   (t
    (print-symbol-in-tptp-format x))))

(defun print-wff-in-tptp-format (wff &optional subst)
  (dereference
   wff subst
   :if-variable (print-term-in-tptp-format wff)
   :if-constant (print-term-in-tptp-format wff)
   :if-compound (cond
                 ((negation-p wff)
                  (cond
                   ((atom-p (arg1 wff))
                    (print-term-in-tptp-format (arg1 wff) subst t))
                   (t
                    (princ "~")
                    (princ "(")
                    (print-wff-in-tptp-format (arg1 wff) subst)
                    (princ ")"))))
                 ((disjunction-p wff)
                  (princ "(") (print-wffs-in-tptp-format (args wff) subst " | ") (princ ")"))
                 ((conjunction-p wff)
                  (princ "(") (print-wffs-in-tptp-format (args wff) subst " & ") (princ ")"))
                 ((equivalence-p wff)
                  (princ "(") (print-wffs-in-tptp-format (args wff) subst " <=> ") (princ ")"))
                 ((exclusive-or-p wff)
                  (princ "(") (print-wffs-in-tptp-format (args wff) subst " <~> ") (princ ")"))
                 ((implication-p wff)
                  (princ "(") (print-wffs-in-tptp-format (args wff) subst " => ") (princ ")"))
                 ((reverse-implication-p wff)
                  (princ "(") (print-wffs-in-tptp-format (args wff) subst " <= ") (princ ")"))
                 (t
                  (print-term-in-tptp-format wff subst))))
  wff)

(defun print-wffs-in-tptp-format (wffs subst sep)
  (let ((first t))
    (dolist (wff wffs)
      (if first (setf first nil) (princ sep))
      (print-wff-in-tptp-format wff subst))))

(defun print-term-in-tptp-format (term &optional subst neg)
  ;; works for true, false, and atoms too; call with neg true for negated atoms
  (dereference
   term subst
   :if-variable (progn
                  (cl:assert (top-sort? (variable-sort term)))
                  (when neg
                    (princ "~"))
                  (mvlet (((:values i j) (floor (variable-number term) 6)))
                    (princ (char "XYZUVW" j))
                    (unless (= 0 i)
                      (write i :radix nil :base 10))))
   :if-constant (progn
                  (when neg
                    (princ "~"))
                  (cond
                   ((eq true term)
                    (princ "$true"))
                   ((eq false term)
                    (princ "$false"))
                   (t
                    (print-symbol-in-tptp-format (constant-name term)))))
   :if-compound (let ((head (head term)))
                  (cond
                   ((eq *=* head)
                    (let ((args (args term)))
                      (print-term-in-tptp-format (first args) subst)
                      (princ (if neg " != " " = "))
                      (print-term-in-tptp-format (second args) subst)))
                   ((eq *cons* head)
                    (when neg
                      (princ "~"))
                    (princ "[")
                    (print-list-in-tptp-format term subst)
                    (princ "]"))
                   (t
                    (when neg
                      (princ "~"))
                    (print-symbol-in-tptp-format (function-name head))
                    (princ "(")
                    (print-list-in-tptp-format (args term) subst)
                    (princ ")")))))
  term)

(defun print-list-in-tptp-format (l subst)
  (let ((first t))
    (loop
      (cond
       ((dereference l subst :if-compound-cons t)
        (if first (setf first nil) (princ ","))
        (print-term-in-tptp-format (car l) subst)
        (setf l (cdr l)))
       ((null l)
        (return))
       (t
        (princ "|")
        (print-term-in-tptp-format l subst)
        (return))))))

(defun print-symbol-in-tptp-format (x)
  (etypecase x
    (symbol
     (let ((string (symbol-name x))
           (quote t)
           (escape nil)
           (first t))
       (map nil
            (lambda (ch)
              (if first
                  (setf quote (not (lower-case-p ch)) first nil)
                  (unless quote
                    (setf quote (not (or (alphanumericp ch) (eq #\_ ch))))))
              (when quote
                (unless escape
                  (setf escape (or (eql #\\ ch) (eql #\' ch))))))
            string)
       (when quote
         (princ #\'))
       (if escape
           (map nil
                (lambda (ch)
                  (when (or (eq #\\ ch) (eq #\' ch))
                    (princ #\\))
                  (princ ch))
                string)
           (princ string))
       (when quote
         (princ #\')))
     x)
    ((or number string)
     (prin1 x))))

(defun mapnconc-tptp-file-forms (function filespec &key (if-does-not-exist :error) (package *package*))
  (let ((snark-infix-reader::*infix-operators* nil)
        (snark-infix-reader::*prefix-operators* nil)
        (snark-infix-reader::*postfix-operators* nil))
    (declare-tptp-operators)
    (let* ((*package* (find-or-make-package package))
           (tokens (mapnconc-file-lines (lambda (string) (tokenize string :rationalize (input-floats-as-ratios?)))
                                        filespec 
                                        :if-does-not-exist if-does-not-exist))
           (result nil) result-last form)
      (loop
        (cond
         ((null tokens)
          (return result))
         (t
          (multiple-value-setq (form tokens) (tokens-to-lisp tokens))
          (setf form (tptp-to-snark-input form))
          (cl:assert (and (consp form)
                          (or (eq '|fof| (first form))
                              (eq '|cnf| (first form))
                              (and (eq '|input_clause| (first form))
                                   (consp (fourth form))
                                   (eq 'list (first (fourth form)))))))
          (when (eq '|input_clause| (first form))
            (setf form (list* (first form) (second form) (third form) (cons 'or (rest (fourth form))) (cddddr form))))
          (ncollect (funcall function
                             (list 'assertion
                                   (fourth form)
                                   (if (eq '|fof| (first form)) :conc-name :name)
                                   (if (eq '|fof| (first form)) (concatenate 'string (string (second form)) "_row_") (second form))
                                   :reason
                                   (tptp-to-snark-reason (third form) form)))
                    result)))))))

(defun tptp-to-snark-reason (reason &optional form)
  (case reason
    (|axiom| 'assertion)
    (|hypothesis| 'assumption)
    (|negated_conjecture| 'negated_conjecture)
    (|conjecture| (if (eq '|cnf| (first form))
                      (progn (warn "Assuming that ~A is really a negated conjecture." form) 'negated_conjecture)
                      'conjecture))
    (otherwise 'assertion)))

(defun declare-tptp-operators ()
  (declare-operator-syntax "<=>" :xfy 505 'iff)
  (declare-operator-syntax "<~>" :xfy 505 'xor)
  (declare-operator-syntax "=>"  :xfy 504 'implies)
  (declare-operator-syntax "<="  :xfy 504 'implied-by)
  (declare-operator-syntax "&"   :xfy 503 'and)
  (declare-operator-syntax "~&"  :xfy 503 'nand)
  (declare-operator-syntax "|"   :xfy 502 'or)
  (declare-operator-syntax "~|"  :xfy 502 'nor)
;;(declare-operator-syntax "@"   :yfx 501)
  (declare-operator-syntax ":"   :xfy 450 'tptp-colon)
  (declare-operator-syntax "~"   :fy  450 'not)
;;(declare-operator-syntax ">"   :xfy 440)
  (declare-operator-syntax "="   :xfx 405 '=)
  (declare-operator-syntax "!="  :xfx 405 '/=)
;;(declare-operator-syntax "~="  :xfx 405)
  (declare-operator-syntax "!"   :fx  400 'forall)
  (declare-operator-syntax "?"   :fx  400 'exists)
;;(declare-operator-syntax "^"   :fx  400)
;;(declare-operator-syntax ".."  :xfx 400)
  (declare-operator-syntax "++"  :fx  100 'tptp-double-plus)
  (declare-operator-syntax "--"  :fx  100 'not)
;;(declare-operator-syntax "!"   :xf  100)
  (declare-operator-syntax "$"   :fx   99 'tptp-dollar)
  (declare-operator-syntax "$$"  :fx   99 'tptp-double-dollar)
  nil)

(defun tptp-to-snark-input (x)
  (cond
   ((atom x)
    x)
   (t
    (let ((fn (first x)))
      (case fn
        (tptp-double-plus
         ;; (++ p) -> p
         (tptp-to-snark-input (second x)))
        (tptp-colon
         ;; (: (quantifier (list . variables)) form) -> (quantifer variables form)
         (cl:assert (and (consp (second x))
                         (member (first (second x)) '(forall exists))
                         (consp (second (second x)))
                         (eq '$$list (first (second (second x))))))
         (list (first (second x)) (strip-colons (rest (second (second x)))) (tptp-to-snark-input (third x))))
        (tptp-dollar
         ;; ($ true/false) -> true/false
         ;; ($ foo) -> $foo
         ;; ($$ foo) -> $$FOO
         ;; ($ (foo a b)) -> ($foo a b)
         ;; ($$ (foo a b)) -> ($$FOO a b)
         (cond
          ((eq '|true| (second x))
           true)
          ((eq '|false| (second x))
           false)
          ((symbolp (second x))
           (intern (concatenate 'string "$" (symbol-name (second x))) :snark-user))
          ((and (consp (second x)) (symbolp (first (second x))))
           (cons (intern (concatenate 'string "$" (symbol-name (first (second x)))) :snark-user) (tptp-to-snark-input-args (rest (second x)))))
          (t
           (lcons fn (tptp-to-snark-input-args (rest x)) x))))
        (tptp-double-dollar
         (cond
          ((symbolp (second x))
           (intern (concatenate 'string "$$" (string-upcase (symbol-name (second x)))) :snark-user))
          ((and (consp (second x)) (symbolp (first (second x))))
           (cons (intern (concatenate 'string "$$" (string-upcase (symbol-name (first (second x))))) :snark-user) (tptp-to-snark-input-args (rest (second x)))))
          (t
           (lcons fn (tptp-to-snark-input-args (rest x)) x))))
        (otherwise
         (lcons fn (tptp-to-snark-input-args (rest x)) x)))))))

(defun tptp-to-snark-input-args (l)
  (lcons (tptp-to-snark-input (first l))
         (tptp-to-snark-input-args (rest l))
         l))

(defun strip-colons (l)
  ;; (: var type) -> (var type) in quantifier variables
  ;; no transformation yet for (: integer var) or (: integer (: var type))
  (lcons (if (and (consp (first l))
                  (eq 'tptp-colon (first (first l)))
                  (symbolp (second (first l)))
                  (symbolp (third (first l))))
             (rest (first l))
             (first l))
         (strip-colons (rest l))
         l))

(defun read-tptp-term (string &rest options)
  (declare (dynamic-extent options))
  (let ((snark-infix-reader::*infix-operators* nil)
        (snark-infix-reader::*prefix-operators* nil)
        (snark-infix-reader::*postfix-operators* nil))
    (declare-tptp-operators)
    (multiple-value-bind (term rest) (apply #'read-infix-term string (append options (list :rationalize (input-floats-as-ratios?))))
      (values (tptp-to-snark-input term) rest))))

;;; tptp.lisp EOF
